Termination w.r.t. Q proof of /tmp/tmphsUnrL/dup01.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a12(a12(a12(a12(x1)))) → x1
a13(a13(a13(a13(x1)))) → x1
a14(a14(a14(a14(x1)))) → x1
a15(a15(a15(a15(x1)))) → x1
a16(a16(a16(a16(x1)))) → x1
a23(a23(a23(a23(x1)))) → x1
a24(a24(a24(a24(x1)))) → x1
a25(a25(a25(a25(x1)))) → x1
a26(a26(a26(a26(x1)))) → x1
a34(a34(a34(a34(x1)))) → x1
a35(a35(a35(a35(x1)))) → x1
a36(a36(a36(a36(x1)))) → x1
a45(a45(a45(a45(x1)))) → x1
a46(a46(a46(a46(x1)))) → x1
a56(a56(a56(a56(x1)))) → x1
a13(a13(x1)) → a12(a12(a23(a23(a12(a12(x1))))))
a14(a14(x1)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))))
a15(a15(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))
a16(a16(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))))
a24(a24(x1)) → a23(a23(a34(a34(a23(a23(x1))))))
a25(a25(x1)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))))
a26(a26(x1)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))))
a35(a35(x1)) → a34(a34(a45(a45(a34(a34(x1))))))
a36(a36(x1)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))))
a46(a46(x1)) → a45(a45(a56(a56(a45(a45(x1))))))
a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) → x1
a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) → x1
a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) → x1
a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) → x1
a12(a12(a34(a34(x1)))) → a34(a34(a12(a12(x1))))
a12(a12(a45(a45(x1)))) → a45(a45(a12(a12(x1))))
a12(a12(a56(a56(x1)))) → a56(a56(a12(a12(x1))))
a23(a23(a45(a45(x1)))) → a45(a45(a23(a23(x1))))
a23(a23(a56(a56(x1)))) → a56(a56(a23(a23(x1))))
a34(a34(a56(a56(x1)))) → a56(a56(a34(a34(x1))))

Q is empty.

↳ QTRS

  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a12(a12(a12(a12(x1)))) → x1
a13(a13(a13(a13(x1)))) → x1
a14(a14(a14(a14(x1)))) → x1
a15(a15(a15(a15(x1)))) → x1
a16(a16(a16(a16(x1)))) → x1
a23(a23(a23(a23(x1)))) → x1
a24(a24(a24(a24(x1)))) → x1
a25(a25(a25(a25(x1)))) → x1
a26(a26(a26(a26(x1)))) → x1
a34(a34(a34(a34(x1)))) → x1
a35(a35(a35(a35(x1)))) → x1
a36(a36(a36(a36(x1)))) → x1
a45(a45(a45(a45(x1)))) → x1
a46(a46(a46(a46(x1)))) → x1
a56(a56(a56(a56(x1)))) → x1
a13(a13(x1)) → a12(a12(a23(a23(a12(a12(x1))))))
a14(a14(x1)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))))
a15(a15(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))
a16(a16(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))))
a24(a24(x1)) → a23(a23(a34(a34(a23(a23(x1))))))
a25(a25(x1)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))))
a26(a26(x1)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))))
a35(a35(x1)) → a34(a34(a45(a45(a34(a34(x1))))))
a36(a36(x1)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))))
a46(a46(x1)) → a45(a45(a56(a56(a45(a45(x1))))))
a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) → x1
a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) → x1
a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) → x1
a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) → x1
a12(a12(a34(a34(x1)))) → a34(a34(a12(a12(x1))))
a12(a12(a45(a45(x1)))) → a45(a45(a12(a12(x1))))
a12(a12(a56(a56(x1)))) → a56(a56(a12(a12(x1))))
a23(a23(a45(a45(x1)))) → a45(a45(a23(a23(x1))))
a23(a23(a56(a56(x1)))) → a56(a56(a23(a23(x1))))
a34(a34(a56(a56(x1)))) → a56(a56(a34(a34(x1))))

Q is empty.

We use [27] with the following order to prove termination.

Knuth-Bendix order [24] with precedence:

a23₁ > a45₁
a23₁ > a56₁
a12₁ > a45₁
a12₁ > a34₁ > a56₁

and weight map:

a46_1=273
a35_1=641
a45_1=128
a13_1=161
a15_1=929
a34_1=256
a56_1=16
a36_1=785
a14_1=545
a23_1=128
a16_1=1073
a25_1=897
a26_1=1041
a24_1=513
a12_1=16
dummyConstant=1